the_es:ES, e', e:E. Dec((e < e')) 

latex

Definitions	P  Q, x:A. B(x), sender(e), t  T, E, (e < e'), P  Q, Prop, A & B, pred(e), b, A, isrcv(e), first(e), P  Q, P & Q, P  Q, ES, Dec(P), {T}, x. t(x), WellFnd{i}(A;x,y.R(x;y)), False
Lemmas	es-sender-causl, decidable cand, decidable not, decidable assert, decidable es-E equal, es-pred-causl, es-causl-wellfnd, es-E wf, decidable wf, event system wf, decidable functionality, es-causl-iff, not wf, es-first wf, assert wf, es-isrcv wf, decidable or, es-pred wf, es-causl wf, es-sender wf